1. Technical Field
The present invention relates to concurrent system verification and more particularly to systems and methods for program verification using peephole partial order reduction with guarded independence relations.
2. Description of the Related Art
Verifying multi-threaded programs is a difficult problem due to the potentially large number of interleavings of transitions from different threads. In explicit-state model checking, partial order reduction (POR) techniques have been be used to exploit the equivalence of interleavings of independent transitions in order to reduce the search state space. Since deciding whether two transitions are dependent may be as hard as solving the verification problem itself, existing methods based on persistent sets (including stubborn sets) or sleep sets often need to use a static analysis to precompute dependent transitions in a conservative (hence less precise) way.
Dynamic partial order reduction lifts the need for applying static analysis a priori by computing persistent sets on-the-fly with dynamic collision detection. The method performs a stateless search and is restricted to cycle-free systems; extending it to a stateful search and combining it with symbolic methods have proven to be difficult.
A major strength of symbolic methods such as SAT-based bounded model checking (BMC) is that, property dependent search space reduction is automatically exploited inside the Boolean or propositional satisfiability (SAT) or Satisfiability Modulo Theories (SMT) solver through the addition of conflict clauses and non-chronological backtracking. In practice, symbolic methods are more efficient than explicit-state methods in handling data (e.g., variables with large domains). Explicit-state model checking does not benefit from the aforementioned reduction brought by the SAT and SMT solvers. Combining persistent-set based methods (and explicit-state reduction methods in general) with symbolic model checking is not an easy task.
The difficulty arises from the fact that explicit-state model checking inspects concrete states individually, while symbolic methods typically manipulate a large set of states implicitly. In particular, transitions that are dynamically independent with respect to a set of paths are much harder to capture and to exploit than transitions that are dynamically independent with respect to a single path.
In FIG. 1, for example, two concurrently running threads access a global array α, and the two pointers p and q may be aliased. Thread T1 has three transitions tAtBtC. Thread T2 has three transitions tαtβtγ. Statically, tA,tB may have conflicts with tα,tβ. However, if in some execution paths (i≠j) holds, then tA,tB and tα,tβ become independent transitions, meaning that the two execution sequences tA;tB;tα;tβ; tC;tγ; and tα;tβ;tA;tB;tC; tγ; are equivalent. Unfortunately, this information cannot be captured by existing symbolic partial order reduction methods. For example, the conventional methods can detect and exploit the above equivalent interleavings if i=foo( ) and j=bar( ) are replaced by i=1 and j=2, but not in the general case.
In explicit-state model checking, traditional partial order reduction methods that rely on a conservative static analysis are unlikely to exploit such conditional equivalence. Dynamic partial order reduction remedies this by detecting conflicts on-the fly. At each concrete state inside the adaptive search, the value of i and j (as well as p and q) are fully determined, making it much easier to detect conflicts (with respect to a particular path). However, it is not easy to directly combine this technique (based on the notion of happens-before) with symbolic encoding.
For symbolic algorithms, missing out on these kinds of dynamic partial-order reductions can be costly, since the model checker needs to exhaustively search the reduced set executions. Suppose a multi-threaded program P has n threads where each thread executes at most k steps. Then the total number of executions of P may be as large as (nk)!/(kl)n>=(nl)k. For the running example, we can capture all the possible interleavings using the lattice structure in FIG. 2. Let trans={tA;tB;tC;tα;tβ;tγ;} be the set of transitions in the two threads. Each vertex of the lattice represents a distinct subset of trans, consisting of the transitions that are already executed. The set of vertices forms a powerset 2Q; the top vertex is { } and the bottom vertex is {tA;tB;tC;tα;tβ;tγ;}. A path from top to bottom denotes a unique interleaving. For example, the left-most line corresponds to tA;tB;tC;tα;tβ;tγ;.
In concurrent systems, the number of interleaving of transitions from different threads or processes can be very large. Existing partial order reduction methods for pruning redundant interleaving during verification are not accurate enough and not suited for symbolic implementation.